/**
 * 
 */
package edu.arizona.bio5.onto.decomposition.locality;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Set;

import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLClassExpression;
import org.semanticweb.owlapi.model.OWLClassExpressionVisitor;
import org.semanticweb.owlapi.model.OWLDataAllValuesFrom;
import org.semanticweb.owlapi.model.OWLDataExactCardinality;
import org.semanticweb.owlapi.model.OWLDataHasValue;
import org.semanticweb.owlapi.model.OWLDataMaxCardinality;
import org.semanticweb.owlapi.model.OWLDataMinCardinality;
import org.semanticweb.owlapi.model.OWLDataSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLEntity;
import org.semanticweb.owlapi.model.OWLObjectAllValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectComplementOf;
import org.semanticweb.owlapi.model.OWLObjectExactCardinality;
import org.semanticweb.owlapi.model.OWLObjectHasSelf;
import org.semanticweb.owlapi.model.OWLObjectHasValue;
import org.semanticweb.owlapi.model.OWLObjectIntersectionOf;
import org.semanticweb.owlapi.model.OWLObjectMaxCardinality;
import org.semanticweb.owlapi.model.OWLObjectMinCardinality;
import org.semanticweb.owlapi.model.OWLObjectOneOf;
import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom;
import org.semanticweb.owlapi.model.OWLObjectUnionOf;

import uk.ac.manchester.cs.util.SetUtils;

import com.clarkparsia.owlapi.modularity.locality.LocalityClass;

/**
 * Given a locality class "x" and a signature S, computes all
 * minimal (w.r.t. inclusion) subsets of S s.t. the given class expression C
 * does not belong to Bot(S)
 * See the paper "Which kind of module should I extract" by T. Schneider et al.
 * 
 * @author Pavel Klinov
 *
 */
public class BottomNonEquivFinder implements OWLClassExpressionVisitor {

	private LocalityClass m_localClass = null;
	private Collection<Set<OWLEntity>> m_minSubsigs = null;
	private Collection<? extends OWLEntity> m_sig = null;
	
	BottomNonEquivFinder(LocalityClass lClass) {
		
		m_localClass  = lClass;
	}
	
	/*
	 * This method should not be called recursively on the same instance (create another instance instead)
	 */
	public Collection<Set<OWLEntity>> findMinimalSignatures(OWLClassExpression clazz, Collection<? extends OWLEntity> signature) {
		
		m_sig = signature;
		m_minSubsigs = new ArrayList<Set<OWLEntity>>();
		clazz.accept(this);
		
		return m_minSubsigs;
	}

	@Override
	public void visit(OWLClass desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        	
        	if (!desc.isOWLNothing()) {//Otherwise the class is in Bot
        		
        		if (!desc.isOWLThing()) {
        			// Need signatures that contain the name of the class
        			LocalityUtils.saveName(desc, m_sig, m_minSubsigs);
        			
        		} else LocalityUtils.saveEmptySignature(m_minSubsigs);
        	}
            break;
        case TOP_BOTTOM:
        case TOP_TOP:
        	
        	if (!desc.isOWLNothing()) LocalityUtils.saveEmptySignature(m_minSubsigs);
		}
	}

	@Override
	public void visit(OWLObjectIntersectionOf desc) {
		//TODO Optimize. Need a data structure to maintain all sets minimal w.r.t. inclusion (i.e., incomparable)
		m_minSubsigs = null;
		// *All* conjuncts must not be in Bot(S)
		for (OWLClassExpression conj : desc.getOperands()) {

			Collection<Set<OWLEntity>> minSigsForConjunct = new BottomNonEquivFinder(m_localClass).findMinimalSignatures(conj, m_sig);
			// Combine the new signatures with signatures that push the previous conjuncts out of Bot(S)
			m_minSubsigs = m_minSubsigs == null ? minSigsForConjunct : SetUtils.unionAllAndMinimizeWrtInclusion(m_minSubsigs, minSigsForConjunct);
			
			if (m_minSubsigs.isEmpty()) break;
		}
	}

	@Override
	public void visit(OWLObjectUnionOf desc) {
		// Save signatures that push at least one disjunct out of Bot(S)
		for (OWLClassExpression conjunct : desc.getOperands()) {
			// Find minimal subsignatures recursively for each disjunct 
			Collection<Set<OWLEntity>> minSigsForDisjunct = new BottomNonEquivFinder(m_localClass).findMinimalSignatures(conjunct, m_sig);
			
			SetUtils.addAllandMinimizeWrtInclusion(minSigsForDisjunct, m_minSubsigs);
		}
	}

	@Override
	public void visit(OWLObjectComplementOf desc) {
		// Save signatures that push the operand out of Top
		m_minSubsigs = new TopNonEquivFinder(m_localClass).findMinimalSignatures(desc.getOperand(), m_sig);
	}

	@Override
	public void visit(OWLObjectSomeValuesFrom desc) {

		BottomNonEquivFinder botNonEqFinder = new BottomNonEquivFinder(m_localClass);
		
		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// All subsignatures S which the contain the property's name and push the filler out of Bot(S)
        	Collection<Set<OWLEntity>> minSigsForFiller = botNonEqFinder.findMinimalSignatures(desc.getFiller(), m_sig);
        	
        	m_minSubsigs = 	SetUtils.unionAndMinimizeWrtInclusion(
        						minSigsForFiller, LocalityUtils.getSingletonSignature(desc.getProperty().getNamedProperty()));
            break;
        case TOP_TOP:
        	//All subsignatures that push the filler out of Bot
        	SetUtils.addAllandMinimizeWrtInclusion(botNonEqFinder.findMinimalSignatures(desc.getFiller(), m_sig), m_minSubsigs);
            break;
		}
	}

	@Override
	public void visit(OWLObjectAllValuesFrom desc) {

		 switch (m_localClass) {
         case BOTTOM_BOTTOM:
         case TOP_BOTTOM:
        	 // The class is never in Bot(S) here
        	 LocalityUtils.saveEmptySignature(m_minSubsigs);
             break;
         case TOP_TOP:
        	// All subsignatures S which either contain the property's name OR push the filler out of Bot
        	SetUtils.addAllandMinimizeWrtInclusion(new BottomNonEquivFinder(m_localClass).findMinimalSignatures(desc.getFiller(), m_sig), m_minSubsigs);

         	if (m_sig.contains(desc.getProperty().getNamedProperty())) {
             	// Add the singleton for the property name        		
         		SetUtils.addAndMinimizeWrtInclusion(LocalityUtils.getSingletonSignature(desc.getProperty().getNamedProperty()), m_minSubsigs);
         	}

             break;
		 }
	}

	@Override
	public void visit(OWLObjectHasValue desc) {

        switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	// All signatures S which contain the property's name
        	LocalityUtils.saveName(desc.getProperty().getNamedProperty(), m_sig, m_minSubsigs);
            break;
        case TOP_TOP:
        	// The class is never in Bot(S) here
       	 	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        }		
	}

	@Override
	public void visit(OWLObjectMinCardinality desc) {

		BottomNonEquivFinder botNonEqFinder = new BottomNonEquivFinder(m_localClass);
		
		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	
        	if (desc.getCardinality() == 0) {
        		//Never in Bot here
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        		
        	} else {
            	//All signatures S s.t:
            	//S contains the property's name
        		//AND
        		//the filler is not in Bot(S)
             	if (m_sig.contains(desc.getProperty().getNamedProperty())) {
             		
             		Collection<Set<OWLEntity>> minSigs = botNonEqFinder.findMinimalSignatures(desc.getFiller(), m_sig);
                 	// Add the singleton for the property name        		
             		m_minSubsigs = SetUtils.unionAndMinimizeWrtInclusion(minSigs, LocalityUtils.getSingletonSignature(desc.getProperty().getNamedProperty()));
             	}
        	}
            break;
        case TOP_TOP:
        	
        	if (desc.getCardinality() == 0) {
        		//Never in Bot here
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        		
        	} else {
            	//All signatures S s.t. the filler is not in Bot(S)
        		m_minSubsigs = botNonEqFinder.findMinimalSignatures(desc.getFiller(), m_sig);
        	}
            break;
		}		
	}

	@Override
	public void visit(OWLObjectExactCardinality desc) {
		//TODO Think how to merge subsignatures for >=nR.C and <=nR.C
		BottomNonEquivFinder botNonEqFinder = new BottomNonEquivFinder(m_localClass);
		
		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	
        	if (desc.getCardinality() == 0) {
        		
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        		
        	} else {
        		// All signatures S s.t.
        		// S contains the property's name
        		// AND
        		// the filler is not in Bot(S)
        		if (m_sig.contains(desc.getProperty().getNamedProperty())) {
             		
             		Collection<Set<OWLEntity>> minSigs = botNonEqFinder.findMinimalSignatures(desc.getFiller(), m_sig);
                 	// Add the singleton for the property name        		
             		m_minSubsigs = SetUtils.unionAndMinimizeWrtInclusion(minSigs, LocalityUtils.getSingletonSignature(desc.getProperty().getNamedProperty()));
             	}
        	}
            break;
        case TOP_TOP:
        	// All signatures S s.t. (the filler is not in Bot(S) or n == 0)
        	// AND
        	// (S contains the property's name OR the filler is not in Top(S))
        	// First, find all those satisfying the second condition
        	m_minSubsigs = new TopNonEquivFinder(m_localClass).findMinimalSignatures(desc.getFiller(), m_sig);

         	if (m_sig.contains(desc.getProperty().getNamedProperty())) {
             	// Add the singleton for the property name        		
         		SetUtils.addAndMinimizeWrtInclusion(LocalityUtils.getSingletonSignature(desc.getProperty().getNamedProperty()), m_minSubsigs);
         	}
         	//Now find those which satisfy the first
        	if (desc.getCardinality() >= 0) {
        		//Need to union with those which push the filler out of Bot(S)
        		Collection<Set<OWLEntity>> minBotSigs = botNonEqFinder.findMinimalSignatures(desc.getFiller(), m_sig);
        			
        		m_minSubsigs = SetUtils.unionAllAndMinimizeWrtInclusion(m_minSubsigs, minBotSigs);
        		
        	} else {
        		
        		m_minSubsigs.clear();
        	}

         	break;
		}
	}

	@Override
	public void visit(OWLObjectMaxCardinality desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	//Never in Bot here
    		LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	
        	if (desc.getCardinality() == 0) {
        		
        		LocalityUtils.saveEmptySignature(m_minSubsigs);
        		
        	} else {
        		// All signatures S s.t.
        		// S contains the property's name
        		// OR
        		// the filler is in Top(S)
        		m_minSubsigs = new TopNonEquivFinder(m_localClass).findMinimalSignatures(desc.getFiller(), m_sig);

             	if (m_sig.contains(desc.getProperty().getNamedProperty())) {
                 	// Add the singleton for the property name        		
             		SetUtils.addAndMinimizeWrtInclusion(LocalityUtils.getSingletonSignature(desc.getProperty().getNamedProperty()), m_minSubsigs);
             	}
        	}
            break;
		}
	}

	@Override
	public void visit(OWLObjectHasSelf desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	
        	LocalityUtils.saveName(desc.getProperty().getNamedProperty(), m_sig, m_minSubsigs);

            break;
        case TOP_TOP:
        	LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
		}
	}

	@Override
	public void visit(OWLObjectOneOf desc) {
		if (!desc.getIndividuals().isEmpty()) {
			//Here it's always not in Bot(S)
			LocalityUtils.saveEmptySignature(m_minSubsigs);
		}
		//Otherwise it's always in Bot(S), so return the empty collection
	}

	@Override
	public void visit(OWLDataSomeValuesFrom desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	//The signatures must contain the property
        	LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
            break;
        case TOP_TOP:
			//Here it's always not in Bot(S)
			LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
    }
	}

	@Override
	public void visit(OWLDataAllValuesFrom desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	//Here it's always not in Bot(S)
			LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	
        	if (desc.getFiller().isTopDatatype()) {
        		//Here it's always not in Bot(S)
    			LocalityUtils.saveEmptySignature(m_minSubsigs);
    			
        	} else {
        		//The signatures must contain the property
            	LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        	}

            break;
		}
	}

	@Override
	public void visit(OWLDataHasValue desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	//The signatures must contain the property
        	LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
            break;
        case TOP_TOP:
        	//Here it's always not in Bot(S)
			LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
		}
	}

	@Override
	public void visit(OWLDataMinCardinality desc) {

		 switch (m_localClass) {
         case BOTTOM_BOTTOM:
         case TOP_BOTTOM:
        	 
        	 if (desc.getCardinality() == 0) {
        		//Here it's always not in Bot(S)
      			LocalityUtils.saveEmptySignature(m_minSubsigs);
      			
        	 } else {
        		//The signatures must contain the property
             	LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        	 }

             break;
         case TOP_TOP:
        	//Here it's always not in Bot(S)
 			LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
		 }
	}

	@Override
	public void visit(OWLDataExactCardinality desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
            
        	if (desc.getCardinality() == 0) {
        		//Here it's always not in Bot(S)
     			LocalityUtils.saveEmptySignature(m_minSubsigs);
     			
        	} else {
        		//The signatures must contain the property
             	LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        	}
            break;
        case TOP_TOP:
        	
        	if (desc.getCardinality() == 0) {
        		
        		if (!LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller())) {
        			//Here it's always not in Bot(S)
         			LocalityUtils.saveEmptySignature(m_minSubsigs);
         			
        		} else {
        			
        			LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        		}
        		
        	} else if (desc.getCardinality() > 0) {
        		
        		if (!LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller())) {
        			//Here it's always not in Bot(S)
         			LocalityUtils.saveEmptySignature(m_minSubsigs);
         			
        		} else {
        			
        			LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        		}
        	}
/*        	
            isBottomEquivalent = 
            	(
            			(
            					(desc.getCardinality() == 0)
            					&& (
            							(!signature.contains(desc.getProperty().asOWLDataProperty())
            						)
            					&& LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))
            			)
            			||
            			(
            					(desc.getCardinality() > 0)
            					&& (
            							(!signature.contains(desc.getProperty().asOWLDataProperty())
            						)
            					&& LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller())
            					)
            			)
            	);*/
            break;
		}
	}

	@Override
	public void visit(OWLDataMaxCardinality desc) {

		switch (m_localClass) {
        case BOTTOM_BOTTOM:
        case TOP_BOTTOM:
        	//Here it's always not in Bot(S)
 			LocalityUtils.saveEmptySignature(m_minSubsigs);
            break;
        case TOP_TOP:
        	
        	boolean topBuiltIn = LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller());
        	
        	if (desc.getCardinality() == 0 || desc.getCardinality() == 1) {
        		
        		if (!topBuiltIn) {
        			//Here it's always not in Bot(S)
         			LocalityUtils.saveEmptySignature(m_minSubsigs);
         			
        		} else {
        			
        			LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        		}
        	} else if (desc.getCardinality() > 1) {
        		
        		if (!LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller())) {
        			//Here it's always not in Bot(S)
         			LocalityUtils.saveEmptySignature(m_minSubsigs);
         			
        		} else {
        			
        			LocalityUtils.saveName(desc.getProperty().asOWLDataProperty(), m_sig, m_minSubsigs);
        		}
        	}
        	
        	/*isBottomEquivalent = (desc.getCardinality() == 0 && !signature.contains(desc.getProperty().asOWLDataProperty()) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))
        						|| (desc.getCardinality() == 1 && !signature.contains(desc.getProperty().asOWLDataProperty()) && LocalityUtils.isTopOrBuiltInDatatype(desc.getFiller()))
        						|| (desc.getCardinality() > 1 && !signature.contains(desc.getProperty().asOWLDataProperty()) && LocalityUtils.isTopOrBuiltInInfiniteDatatype(desc.getFiller()));*/
            break;
		}
	}
}
